Step of Proof: int_lt_to_int_upper 9,38

Inference at * 1 
Iof proof for Lemma int lt to int upper:



  i:A:({i + 1...}). (j:. (i < j A(j))  (j:{i + 1...}. A(j)) 
latex

 by ((GenUnivCD) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 
latex


C1

C1: 1. i : 
C1: 2. A : {i + 1...}
C1: 3. j:. (i < j A(j)
C1: 4. j : {i + 1...}
C1:   A(j)
C2

C2: 1. i : 
C2: 2. A : {i + 1...}
C2: 3. j:{i + 1...}. A(j)
C2: 4. j : 
C2: 5. i < j
C2:   A(j)
C.


DefinitionsFalse, A, A  B, t  T, P  Q, P  Q, x(s), P  Q, P  Q, , {i...}, x:AB(x)
Lemmasle wf, int upper wf

origin